Thực đơn
Các phương pháp hình thức Phân loạiCác phương pháp hình thức có thể được sử dụng tại nhiều mức:
Mức 0: Đặc tả hình thức có thể được thực hiện và rồi một chương trình được phát triển từ đặc tả này một cách không hình thức. Trong nhiều trường hợp, cách này có thể là lựa chọn hiệu quả nhất về mặt chi phí.
Mức 1: Sử dụng phát triển và kiểm định hình thức để tạo một chương trình theo một quy trình hình thức hơn. Ví dụ, có thể thực hiện các chứng minh về các tính chất hoặc quá trình tinh chỉnh (refinement) từ đặc tả hình thức tới một chương trình. Đây có thể là lựa chọn phù hợp nhất đối với các hệ thống yêu cầu tính toàn vẹn cao với các tiêu chí về an toàn và an ninh.
Mức 2: Sử dụng các bộ chứng minh định lý (theorem prover) để thực hiện các chứng minh hình thức hoàn toàn và được kiểm chứng bằng máy móc. Việc này có thể đòi hỏi chi phí rất cao và chỉ đáng lựa chọn trong thực tiễn nếu phí tồn cho các lỗi sai là cực kỳ cao (ví dụ, trong các phần quan trọng của thiết kế bộ vi xử lý).
Cùng với ngành con Ngữ nghĩa hình thức của ngôn ngữ lập trình, các phương pháp hình thức có thể được phân loại tương đối như sau:
Thực đơn
Các phương pháp hình thức Phân loạiLiên quan
Các Tiểu vương quốc Ả Rập Thống nhất Các dân tộc tại Việt Nam Cách mạng Công nghiệp Các trận đấu trong Đường lên đỉnh Olympia năm thứ 24 Cách mạng Tháng Tám Cục Điều tra Liên bang Cực quang Cốc Cốc Cục Cảnh sát điều tra tội phạm về tham nhũng, kinh tế, buôn lậu Cục Dự trữ Liên bang (Hoa Kỳ)Tài liệu tham khảo
WikiPedia: Các phương pháp hình thức http://home0.inet.tele.dk/pgl/fmtrends98.pdf http://people.csail.mit.edu/dnj/publications/alloy... http://people.csail.mit.edu/dnj/publications/ieee9... http://vl.fmnet.info/ http://vl.fmnet.info/companies/ http://vl.fmnet.info/meetings/ http://vl.fmnet.info/orgs/ http://vl.fmnet.info/pubs/ http://vl.fmnet.info/whos-who/ http://www.stsc.hill.af.mil/crosstalk/2003/01/Geor...